A:Type, eq:EqDecider(A), B:(AType), f:fpf(A; x.B(x)),
P:(x:{x:A| fpf-dom(eq; x; f)} B(x)prop{i:l}). fpf-all(A; eq; f; x,v.P(x,v))  prop{i:l} 

latex

Definitions	x:A. B(x), x(s), prop{i:l}, t  T, fpf-all(A; eq; f; x,v.P(x;v)), x(s1,s2), P  Q, x. t(x)
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-ap wf, fpf wf, deq wf